Nuprl Lemma : normal-ds-single
11,40
postcript
pdf
x
:Id,
T
:Type. normal-type{i:l}(
T
)
normal-ds{i:l}(fpf-single(
x
;
T
))
latex
Definitions
normal-type{i:l}(
T
)
,
atom{$n:n}
,
Id
,
s
=
t
,
guard(
T
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
sq_type(
T
)
,
t
T
,
sqequal(
s
;
t
)
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
fpf-single(
x
;
v
)
,
fpf-ap(
f
;
eq
;
x
)
,
b
,
fpf-all(
A
;
eq
;
f
;
x
,
v
.
P
(
x
;
v
))
,
normal-ds{i:l}(
ds
)
,
Type
Lemmas
fpf-single-dom
,
Id
sq
origin
x:Id, T:Type. normal-type{i:l}(T) 
normal-ds{i:l}(fpf-single(x; T)) x:Id, T:Type. normal-type{i:l}(T) normal-ds{i:l}(fpf-single(x; T)) Qx:A. B(x)
T
B(x)
B(x)
Q
Q
b